This article answers two questions (posed in the literature), each concerningthe guaranteed existence of proofs free of double negation. A proof is free ofdouble negation if none of its deduced steps contains a term of the formn(n(t)) for some term t, where n denotes negation. The first question asks forconditions on the hypotheses that, if satisfied, guarantee the existence of adouble-negation-free proof when the conclusion is free of double negation. Thesecond question asks about the existence of an axiom system for classicalpropositional calculus whose use, for theorems with a conclusion free of doublenegation, guarantees the existence of a double-negation-free proof. Aftergiving conditions that answer the first question, we answer the second questionby focusing on the Lukasiewicz three-axiom system. We then extend our studiesto infinite-valued sentential calculus and to intuitionistic logic andgeneralize the notion of being double-negation free. The double-negation proofsof interest rely exclusively on the inference rule condensed detachment, a rulethat combines modus ponens with an appropriately general rule of substitution.The automated reasoning program OTTER played an indispensable role in thisstudy.
展开▼
